Nuprl Lemma : map_length_nat
4,23
postcript
pdf
A
,
B
:Type,
f
:(
A
B
),
as
:
A
List. ||map(
f
;
as
)|| = ||
as
||
latex
Definitions
x
:
A
.
B
(
x
)
,
||
as
||
,
t
T
,
map(
f
;
as
)
,
P
Q
,
False
,
A
,
A
B
,
Lemmas
map
wf
,
length
wf1
origin
A, B:Type, f:(A
B), as:A List. ||map(f;as)|| = ||as|| 
A, B:Type, f:(AB), as:A List. ||map(f;as)|| = ||as|| x:A. B(x) T
Q
A
B